I grew increasingly unhappy with the short-comings the initial version, and therefore set out to write an STM test addressing some of them in ef4b42d.

The resulting STM test

• runs the two test properties in a child Domain (to avoid Domain.DLS polution across repetitions) and
• allocates an initial list of keys as suggested

I also adjusted the Util.repeat and retries parameters as a lot repetition didn't seem necessary to trigger it, and since I needed to write out the properties anyway to run the test properties in a child Domain.

This results in a negative test, that is quickly able to produce a counterexample where simultanious changes in two children are not seen in the sibling:

  Results incompatible with linearized model

                               |                           
                               |                           
            .------------------------------------.
            |                                    |                           
     Set (2, 1) : ()                      Set (0, 43) : ()                   
        Get 0 : 0                            Get 2 : 2            

A round of focused tests confirmed that the STM Domain.DLS test runs fast and works reasonable well.
I've therefore disabled the initial Lin test.

I expect this full CI run to fail its trunk workflows without #12545 merged into ocaml/ocaml.

CI summary

• all 17 trunk/5.2 workflows failed during opam install qcheck-core which has been reported and fixed upstream
• 2 MingW bytecode 5.1 timedout during threadomain [ocaml5-issue] Windows failures on threadomain #203

Out of 59 workflows and 19 failures, the 2 non-trunk failures were thus genuine.
I'll merge.